\begin{tabbing}
es{-}send{-}atom{-}to(${\it es}$;$e$;$a$;$i$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=alle{-}at(${\it es}$;$i$;${\it e'}$.($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))\+
\\[0ex]$\Rightarrow$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$))
\\[0ex]$\Rightarrow$ free{-}from{-}atom\{1\}(es{-}valtype(${\it es}$; ${\it e'}$);es{-}val(${\it es}$; ${\it e'}$);$a$))
\-
\end{tabbing}